#include <iostream>
#include <stack>
#include <vector>
#include <fstream>
#include <sstream>
#include <string>
#include <algorithm>

using namespace std;

int clock = 1;

// Arbitrary string
const string  ARBITRARY_STRING = "--";


// Deprecated
enum ALLSTATES {
		// Noncritical
		N1, N2, NN1, NN2,
		// Critical
		C1, C2, NC1, NC2, 
		// Trying
		T1, T2, NT1, NT2};

// Mutual Exclusion
struct state {
	string s1, s2;
	string prefix, connector;
	
	state() {}
	state(string one, string two) {
		s1 = one;
		s2 = two;
	}
	bool isSatisfy(string o, string t);
	bool isSatisfy(string o, string t, string logicOperator);
	bool isSatisfy(state s);
};

bool state::isSatisfy(string o, string t) 
{
	if ((o == s1 && t == s2) || (o == s2 && t == s1))
		return true;
	return false;
}

bool state::isSatisfy(string o, string t, string logicOperator) 
{
	if ((o == s1 && t == s2) || (o == s2 && t == s1))
		return true;
	return false;
}

bool state::isSatisfy(state s) 
{
	bool result = false;
	if (s.connector == "&&") {
		if (s.s1 == ARBITRARY_STRING && s.s2 == ARBITRARY_STRING) {
			result = true;
		} else if (s.s1 == ARBITRARY_STRING) {
			if (s.s2 == s2 || s.s2 == s1)
				result = true;
		} else if (s.s2 == ARBITRARY_STRING) {
			if (s.s1 == s2 || s.s1 == s1)
				result = true;
		} else {
			if ((s.s1 == s1 && s.s2 == s2) || (s.s1 == s2 && s.s2 == s1)) {
				result = true;
			}
		}		
	} else {
		if ((s.s1 == s1 || s.s2 == s2) || (s.s1 == s2 || s.s2 == s1)) {
			result = true;
		}
	}

	if (!s.prefix.empty())
		result = !result;
	return result;
}

struct vertex {
	struct edge **edges, **reversedEdges;
	int numberOfEdges;
	int numberOfReversedEdges;
	int id;
	// Be visited or not
	bool visited;
	// Be popuped or not
	bool popuped;

	// Preorder and postorder
	int preorder, postorder;

	// Belong to a path which contains a vertex satisfying a specific state
	bool isBelongSPath;

	state s;

	vertex() {
		edges = NULL;
		numberOfEdges = numberOfReversedEdges = 0;
		visited = false;
		popuped = false;
		preorder = postorder = -1;
		isBelongSPath = false;
	}

	vertex(int identity, int maximalNumberOfEdges) {
		edges = new struct edge* [maximalNumberOfEdges];
		reversedEdges = new struct edge* [maximalNumberOfEdges];
		id = identity;
		numberOfEdges = numberOfReversedEdges = 0;
		visited = false;
		popuped = false;
		preorder = postorder = -1;
		isBelongSPath = false;
	}

	bool addEdge(struct edge* e);
	bool addReversedEdge(struct edge *re);
	void restoreStates(void);
	void toString(void);
};

// The counterexample
vertex* counterexample = NULL;
// The counterexamples for EG
vector<vertex*> counterexamples;

struct edge {
	struct vertex* start;
	struct vertex* end;

	edge () {
		start = end = NULL;
	}

	edge (struct vertex* s, struct vertex* e) {
		start = s;
		end = e;
	}
};

bool vertex::addEdge(struct edge* e)
{
		if (e->start != this)
			return false;

		edges[numberOfEdges++] = e;
		return true;
}	

bool vertex::addReversedEdge(struct edge* re)
{
		if (re->start != this)
			return false;

		reversedEdges[numberOfReversedEdges++] = re;
		return true;
}	

void vertex::restoreStates(void)
{
	visited = false;
	popuped = false;
	postorder = preorder = -1;
	isBelongSPath = false;
}

void vertex::toString(void)
{
	printf("ID: %d States: %s %s\n", id, s.s1.c_str(), s.s2.c_str());
}

bool previsit(vertex *v, state s) 
{
	return v->s.isSatisfy(s);
}

/*
 * Explore the graph from the vertex {@link #v} iterativelly
 * Require: a vertex v, the entry point of the exploration
 */
void explore(vertex *v) 
{	
	v->visited = true;
	int numberOfEdges = v->numberOfEdges;
	// Previsit (vertexIndex)
	//printf("%d\t%d\n", v->id, clock);
	++clock;
	for (int i = 0; i < numberOfEdges; i++) {
		if (!v->edges[i]->end->visited) {
			explore(v->edges[i]->end);
		}
	}
	//printf("%d\t%d\n", v->id, clock);
	++clock;
	// Postvisit (vertexIndex)
}

/*
 * Explore the graph from the vertex {@link #v} non-iterativelly
 * Require: a vertex v, the entry point of the exploration
 */
void noniterativeExplore(vertex *v) 
{
	stack<vertex*> stc;
	stc.push(v);
	vertex *temp;
	int numberOfEdges;
	while (!stc.empty()) {
		temp = stc.top();
		if (!temp->visited) {
			temp->visited = true;

			numberOfEdges = temp->numberOfEdges;

			//printf("%d\t%d\n", temp->id, clock);
			++clock;
			// Previsit (temp)			
			for (int i = 0; i < numberOfEdges; i++) {
				if (!temp->edges[i]->end->visited) {				
					stc.push(temp->edges[i]->end);
				}
			}
		} else {
			// Postvisit (temp)
			stc.pop(); 
			if (!temp->popuped) {
				temp->popuped = true;
				//printf("%d\t%d\n", temp->id, clock);
				++clock;
			}
		}
	}	
}

// AG
bool noniterativeAlwaysGloballyExplore(vertex *v, state s) 
{
	stack<vertex*> stc;
	stc.push(v);
	vertex *temp;
	int numberOfEdges;
	while (!stc.empty()) {
		temp = stc.top();
		if (!temp->visited) {
			temp->visited = true;

			numberOfEdges = temp->numberOfEdges;

			//printf("%d\t%d\n", temp->id, clock);
			++clock;
			// Previsit (temp)
			if (!previsit(temp, s)) {
				counterexample = temp;
				return false;
			}
 			for (int i = 0; i < numberOfEdges; i++) {
				if (!temp->edges[i]->end->visited) {				
					stc.push(temp->edges[i]->end);
				}
			}

		} else {
			// Postvisit (temp)
			stc.pop(); 
			if (!temp->popuped) {
				temp->popuped = true;
				//printf("%d\t%d\n", temp->id, clock);
				++clock;
			}
		}
	}	
	return true;
}

// AF - Deprecated
bool noniterativeAlwaysFinallyExplore(vertex *v, state s) 
{
	stack<vertex*> stc;
	vector<vertex*> path;
	stc.push(v);
	vertex *temp;
	int numberOfEdges;
	bool canFurther = false;
	bool existSatisfiedVertex = false;
	while (!stc.empty()) {
		temp = stc.top();
		if (!temp->visited) {
			temp->visited = true;

			canFurther = false;
			existSatisfiedVertex = false;

			numberOfEdges = temp->numberOfEdges;

			//printf("%d\t%d\n", temp->id, clock);
			temp->preorder = clock;
			 
			++clock;
			// Previsit @{temp}
			if (previsit(temp, s)) {
				// There is no necessity to go deeper
				existSatisfiedVertex = true;
				temp ->isBelongSPath = true;
				continue;
			}
			
 			for (int i = 0; i < numberOfEdges; i++) {
				if (!temp->edges[i]->end->visited) {				
					stc.push(temp->edges[i]->end);
					canFurther = true;
				} else {
					// edges[i] may be a back edge or cross edge
					if (temp->edges[i]->end->preorder < temp->preorder) {
						if (temp->edges[i]->end->postorder == -1) {
							// @{edges[i]} is a back edge
							return true;
						} else {
							// @{edges[i]} is a cross edge
							// There isn't any probability that a path passing @{temp->edges[i]->end}
							// exists along which every vertex satisfied state @{s}
						}
					}
				}
			}

			if (!canFurther) {
				return false;
			}
		} else {
			// Postvisit (temp)
			stc.pop(); 
			if (existSatisfiedVertex) {
				temp->isBelongSPath = true;
			}
			if (!temp->popuped) {
				temp->popuped = true;
				//printf("%d\t%d\n", temp->id, clock);
				temp->postorder = clock;
				++clock;
			}
		}
	}	
	return true;
}

// AF - iterativelly
bool iterativeAlwaysFinallyExplore(vertex *v, state s) 
{
	v->visited = true;
	if (previsit(v, s))
		return true;

	if (v->numberOfEdges == 0) {
		counterexample = v;
		return false;
	}
	for (int i = 0; i < v->numberOfEdges; i++) {
		vertex* descendant = v->edges[i]->end;
		if (!descendant->visited) {
			if (!iterativeAlwaysFinallyExplore(descendant, s)) {
				return false;
			}
		}
	}
	return true;
}

// EG - deprecated
bool noniterativeExistabilityGloballyExplore(vertex *v, state s) 
{
	stack<vertex*> stc;
	stc.push(v);
	vertex *temp;
	int numberOfEdges;
	
	while (!stc.empty()) {
		temp = stc.top();
		if (!temp->visited) {
			temp->visited = true;

			numberOfEdges = temp->numberOfEdges;

			//printf("%d\t%d\n", temp->id, clock);
			temp->preorder = clock;
			++clock;
			if (previsit(temp, s)) {
				if (numberOfEdges == 0) // Means arriving a leaf node in spanning trees
					return true;
 				for (int i = 0; i < numberOfEdges; i++) {
					if (!temp->edges[i]->end->visited) {						
						stc.push(temp->edges[i]->end);						
					} else {
						// @{edges[i]} may be a back edge or cross edge
						if (temp->edges[i]->end->preorder < temp->preorder) {
							if (temp->edges[i]->end->postorder == -1) {
								// @{edges[i]} is a back edge
								return true;
							} else {
								// @{edges[i]} is a cross edge
								// There isn't any probability that a path passing @{temp->edges[i]->end}
								// exists along which every vertex satisfied state @{s}
							}
						}
					}
				}
			}
		} else {
			// Postvisit (temp)
			stc.pop(); 
			if (!temp->popuped) {
				temp->popuped = true;
				//printf("%d\t%d\n", temp->id, clock);
				temp->postorder = clock;
				++clock;
			}
		}
	}	
	return false;
}

// EG - iterative
bool iterativeExistabilityGloballyExplore(vertex *v, state s) 
{	
	v->visited = true;
	if (!previsit(v, s)) {
		counterexamples.push_back(v);
		return false;
	}

	if (v->numberOfEdges == 0) {
		return true;
	}
	
	bool hasBackEdges = false;
	for (int i = 0; i < v->numberOfEdges; i++) {
		vertex *descendant = v->edges[i]->end;		
		if (!descendant->visited) {			
			if (iterativeExistabilityGloballyExplore(descendant, s))
				return true;
		} else {
			hasBackEdges = true;
		}
	}

	return hasBackEdges;

}

// EF
bool noniterativeExistabilityFinallyExplore(vertex *v, state s) 
{
	stack<vertex*> stc;
	stc.push(v);
	vertex *temp;
	int numberOfEdges;
	
	while (!stc.empty()) {
		temp = stc.top();
		if (!temp->visited) {
			temp->visited = true;

			numberOfEdges = temp->numberOfEdges;

			//printf("%d\t%d\n", temp->id, clock);
			++clock;

			// Previsit {@temp}
			if (previsit(temp, s)) {
				return true;
			} else {
				counterexample = temp;
			}
			for (int i = 0; i < numberOfEdges; i++) {
				if (!temp->edges[i]->end->visited) {						
					stc.push(temp->edges[i]->end);					
				}
			}
		} else {
			// Postvisit (temp)
			stc.pop(); 
			if (!temp->popuped) {
				temp->popuped = true;
				//printf("%d\t%d\n", temp->id, clock);
				++clock;
			}
		}
	}	
	return false;
}

void DFS(vertex **v, int numberOfVertices, int startVertexIndex) 
{
	if (startVertexIndex <= 0 || startVertexIndex > numberOfVertices)
		return;
	vertex* startVertex = v[startVertexIndex];
	for (int i = 1; i <= numberOfVertices; i++) {
		if (!v[i]->visited) 
			noniterativeExplore(v[i]);
	}

}

/* AG: Always Globally
 * 
 * Require: array of vertices representing the graph, and the number of vertices,
 *          and the index of the vertex which is the entry vertex of exploration,
 *			and the state to be checked on.
 * Return: true if all vertices of the graph satisfy {@link #s}, or return false
 */
bool AlwaysGloballyDFS(vertex **v, int numberOfVertices, int startVertexIndex, state s) 
{
	if (startVertexIndex <= 0 || startVertexIndex > numberOfVertices)
		return false;
	for (int i = 1; i <= numberOfVertices; i++) {
		if (!v[i]->visited) {
			if (!noniterativeAlwaysGloballyExplore(v[i], s)) {
				return false;				
			}
		}
	}

	return true;
}


/* AF: Always Finally
 *
 * Require: array of vertices representing the graph, and the number of vertices,
 *          and the index of the vertex which is the entry vertex of exploration,
 *			and the state to be checked on.
 * Return: true if there exists a vertex satisfying {@link #s} in each path starting from the entry vertex
 * 			of the graph, or return false
 */
bool AlwaysFinallyDFS(vertex **v, int numberOfVertices, int startVertexIndex, state s) 
{
	if (startVertexIndex <= 0 || startVertexIndex > numberOfVertices)
		return false;

	return iterativeAlwaysFinallyExplore(v[startVertexIndex], s);
}

/* AX: Always Next
 * Require: array of vertices representing the graph, and the number of vertices,
 *          and the index of the vertex which is the entry vertex of exploration,
 *			and the state to be checked on.
 * Return: true if all child vertices of the entry vertex satisfy {@link #s}, or return false
 */
bool AlwaysNextDFS(vertex **v, int numberOfVertices, int startVertexIndex, state s) 
{
	if (startVertexIndex <= 0 || startVertexIndex > numberOfVertices)
		return false;
	
	vertex* currentVertex = v[startVertexIndex];
	for (int i = 0; i < currentVertex->numberOfEdges; i++) {
		if (!previsit(currentVertex->edges[i]->end, s)) {
			counterexample = currentVertex->edges[i]->end;
			return false;
		}
	}

	return true;

}

/* EG: Existability Globally
 * Require: array of vertices representing the graph, and the number of vertices,
 *          and the index of the vertex which is the entry vertex of exploration,
 *			and the state to be checked on.
 * Return: true if exists a path along which all vertices satisfy {@link #s}, or return false
 */
bool ExistabilityGloballyDFS(vertex **v, int numberOfVertices, int startVertexIndex, state s) 
{
	if (startVertexIndex <= 0 || startVertexIndex > numberOfVertices)
		return false;

	counterexamples.clear();
	return iterativeExistabilityGloballyExplore(v[startVertexIndex], s);
}

/* EF: Existability Finally
 * Require: array of vertices representing the graph, and the number of vertices,
 *          and the index of the vertex which is the entry vertex of exploration,
 *			and the state to be checked on.
 * Return: true if exists one vertex satisfy {@link #s}, or return false
 */
bool ExistabilityFinallyDFS(vertex **v, int numberOfVertices, int startVertexIndex, state s) 
{
	if (startVertexIndex <= 0 || startVertexIndex > numberOfVertices)
		return false;
	
	for (int i = 1; i <= numberOfVertices; i++) {
		if (!v[i]->visited) {
			if (noniterativeExistabilityFinallyExplore(v[i], s)) {
				return true;
			}
		} 
	}

	return false;
}

/* EX: Existability Next
 * Require: array of vertices representing the graph, and the number of vertices,
 *          and the index of the vertex which is the entry vertex of exploration,
 *			and the state to be checked on.
 * Return: true if one child or descendant vertex of the entry vertex satisfy {@link #s}, or return false
 */
bool ExistabilityNextDFS(vertex **v, int numberOfVertices, int startVertexIndex, state s) 
{
	if (startVertexIndex <= 0 || startVertexIndex > numberOfVertices)
		return false;
	
	vertex* currentVertex = v[startVertexIndex];
	for (int i = 0; i < currentVertex->numberOfEdges; i++) {
		if (previsit(currentVertex->edges[i]->end, s)) {
			return true;
		} else {
			counterexample = currentVertex->edges[i]->end;
		}
	}

	return false;
}

// Very naive parsing
bool parseFormula(const string &formula, state &s)
{
	if (formula.empty()) {
		return false;
	}

	if (formula[0] != 'A' && formula[0] != 'E') {
		return false;
	}

	if (formula[1] != 'F' && formula[1] != 'G' && formula[1] != 'X') {
		return false;
	}

	string logicExpression = formula.substr(3, formula.size() - 4);
	if (logicExpression.empty()) {
		return false;
	}
	
	string predicate1, predicate2, connector;
	
	if (logicExpression[0] == '-') { // The symbol of NOT operator
		s.prefix = '-';
		predicate1 = logicExpression.substr(2, 2);
		if (logicExpression[4] == '&' && logicExpression[5] == '&') {
			predicate2 = logicExpression.substr(6, 2);
			connector = "&&";
		} else if (logicExpression[4] == '|' && logicExpression[5] == '|') {
			predicate2 = logicExpression.substr(6, 2);
			connector = "||";
		} else {
			// Wrong logical connector
			return false;
		}
	} else {
		predicate1 = logicExpression.substr(0, 2);
		if (logicExpression[2] == '&' && logicExpression[3] == '&') {
			predicate2 = logicExpression.substr(4, 2);
			connector = "&&";
		} else if (logicExpression[2] == '|' && logicExpression[3] == '|') {
			predicate2 = logicExpression.substr(4, 2);
			connector = "||";
		} else {
			// Wrong logical connector
			printf("Unknown logical connector: %s\n", logicExpression.substr(2,2));
			return false;
		}
	}

	s.s1 = predicate1;
	s.s2 = predicate2;
	s.connector = connector;	

	return true;
}


// Split a string into a vector of substrings
vector<string> split(const string& s, const string& delim, const bool keep_empty = true) {
    vector<string> result;
    if (delim.empty()) {
        result.push_back(s);
        return result;
    }
    string::const_iterator substart = s.begin(), subend;
    while (true) {
        subend = search(substart, s.end(), delim.begin(), delim.end());
        string temp(substart, subend);
        if (keep_empty || !temp.empty()) {
            result.push_back(temp);
        }
        if (subend == s.end()) {
            break;
        }
        substart = subend + delim.size();
    }
    return result;
}

// Is a new map
bool isNewMap(const string& formulaStr) 
{
	vector<string> substrVector = split(formulaStr, " ");
	if (substrVector.size() == 2)
		return true;
	return false;
}

// Extract the number of vertices and edges
void extractNumbers(const string& formulaStr, int &numberOfVertices, int& numberOfEdges)
{
	sscanf(formulaStr.c_str(), "%d %d", &numberOfVertices, &numberOfEdges);
}

// Print counter example for AF and EG
void printCounterExample(vertex *counterexample, int startIndex, state s)
{
	if (counterexample->id == startIndex) {
		counterexample->toString();
		return;
	}

	for (int i = 0; i < counterexample->numberOfReversedEdges; i++) {
		vertex* parent = counterexample->reversedEdges[i]->end;
		if (parent->visited	&& !previsit(parent, s)) {
			counterexample->toString();
			printCounterExample(parent, startIndex, s);
		}
	}
}


int main(int argc, char **argv) 
{
	// Assume the Kripke Structure is stored in the form of a graph G = (V, E)
	int numberOfVertices, numberOfEdges;

	ifstream file("input.in", ios::in);
	if (!file) {
		printf("file input.in not found\n");
		return -1;
	}

	file >> numberOfVertices >> numberOfEdges;
	int numberOfMap = 0;
	while (numberOfVertices != 0 && numberOfEdges != 0) {
		printf("Map %d\n", numberOfMap++);
		vertex **v = new vertex* [numberOfVertices + 1];
		string state1, state2;
		int i;
		for (i = 1; i < (numberOfVertices + 1); i++) {
			file >> state1 >> state2;
			v[i] = new vertex(i, numberOfVertices - 1);
			v[i]->s.s1 = state1;
			v[i]->s.s2 = state2;
			
		}

		int start, end;
		
		for (i = 0; i < numberOfEdges; i++) {
			file >> start >> end;
			edge *e = new edge(v[start], v[end]);
			edge *re = new edge(v[end], v[start]);
			v[start]->addEdge(e);
			v[end]->addReversedEdge(re);
		}
		
		// The formula composed of path operators and the temporal operators
		string formulaStr;
		// Pass the last '\n' character
		getline(file, formulaStr);
		int num = 0;
		while (getline(file, formulaStr)) {
			if (isNewMap(formulaStr))
				break;
			printf("#%d\t%s\n", num, formulaStr.c_str());
			// State parsed from the formula
			state s;

			if (!parseFormula(formulaStr, s)) {
				for (i = 1; i <= numberOfVertices; i++) {
					for (int j = 0; j < v[i]->numberOfEdges; j++) {
						delete v[i]->edges[j];
					}
					delete v[i];
				}
				delete[] v;
				printf("Wrong forms of formulas!\n");
				file.close();
				return -1;
			}

			// Restore states of vertices
			for (i = 1; i <= numberOfVertices; i++) {
				v[i]->restoreStates();
				clock = 1;
			}

			switch (formulaStr[0]) {
				case 'A':
					switch (formulaStr[1]) {
						case 'G':
							if (AlwaysGloballyDFS(v, numberOfVertices, 1, s)) {
								printf("True\n");
							} else {
								// Print a counterexample
								if (counterexample) {
									printf("Counterexample: \n");
									counterexample->toString();
									counterexample = NULL;
								} else {
									printf("Some unexpected problems happened\n");
								}
							}
							break;
						case 'F':
							if (AlwaysFinallyDFS(v, numberOfVertices, 1, s)) {
								printf("True\n");
							} else {
								// Print a counterexample
								if (counterexample) {
									printf("Counterexample: \n");
									printCounterExample(counterexample, 1, s);
								} else {
									printf("Some unexpected problems happened\n");
								}
							}
							break;
						case 'X':
							if (AlwaysNextDFS(v, numberOfVertices, 1, s)) {
								printf("True\n");
							} else {
								if (counterexample) {
									printf("Counterexample: \n");
									counterexample->toString();
									counterexample = NULL;
								} else {
									printf("Some unexpected problems happened\n");
								}
							}
							break;
						default:
							break;
					}
					break;
				case 'E':
					switch (formulaStr[1]) {
						case 'G':
							if (ExistabilityGloballyDFS(v, numberOfVertices, 1, s)) {
								printf("True\n");
							} else {
								if (!counterexamples.empty()) {
									printf("Counterexample: \n");
									vector<vertex*>::const_iterator iter = counterexamples.begin();
									while (iter != counterexamples.end()) {
										vertex* ver = *iter;
										ver->toString();
										++iter;
									}
								} else {
									printf("Some unexpected problems happened\n");
								}
							}
							break;
						case 'F':
							if (ExistabilityFinallyDFS(v, numberOfVertices, 1, s)) {
								printf("True\n");
							} else {
								if (counterexample) {
									printf("Counterexample: \n");
									counterexample->toString();
									counterexample = NULL;
								} else {
									printf("Some unexpected problems happened\n");
								}
							}
							break;
						case 'X':
							if (ExistabilityNextDFS(v, numberOfVertices, 1, s)) {
								printf("True\n");
							} else {
								if (counterexample) {
									printf("Counterexample: \n");
									counterexample->toString();
									counterexample = NULL;
								} else {
									printf("Some unexpected problems happened\n");
								}
							}
						default:
							break;

					}
					break;
				default:
					break;
			}
			++num;
		} // end the while loop
		// Release memory
		for (i = 1; i < (numberOfVertices + 1); i++) {
			for (int j = 0; j < v[i]->numberOfEdges; j++) {
				delete v[i]->edges[j];
			}
			delete v[i];
		}
		delete[] v;

		// Get the new number of vertices and edges
		extractNumbers(formulaStr, numberOfVertices, numberOfEdges);
		printf("\n\n");
	}

	// Close the file
	file.close();
	
	return 0;
}
